Termination w.r.t. Q proof of /tmp/tmptQqJFF/turing

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

1(q0(1(x1))) → 0(1(q1(x1)))
1(q0(0(x1))) → 0(0(q1(x1)))
1(q1(1(x1))) → 1(1(q1(x1)))
1(q1(0(x1))) → 1(0(q1(x1)))
0(q1(x1)) → q2(1(x1))
1(q2(x1)) → q2(1(x1))
0(q2(x1)) → 0(q0(x1))

Q is empty.

↳ QTRS

  ↳ DirectTerminationProof

Q restricted rewrite system:
The TRS R consists of the following rules:

1(q0(1(x1))) → 0(1(q1(x1)))
1(q0(0(x1))) → 0(0(q1(x1)))
1(q1(1(x1))) → 1(1(q1(x1)))
1(q1(0(x1))) → 1(0(q1(x1)))
0(q1(x1)) → q2(1(x1))
1(q2(x1)) → q2(1(x1))
0(q2(x1)) → 0(q0(x1))

Q is empty.

We use [27] with the following order to prove termination.

Knuth-Bendix order [24] with precedence:

q1₁ > 1₁ > 0₁ > q2₁ > q0₁

and weight map:

q1_1=2
1_1=2
q2_1=2
q0_1=2
0_1=2
dummyConstant=1